Termination Proofs by Context-Dependent Interpretations
Identifieur interne : 009271 ( Main/Exploration ); précédent : 009270; suivant : 009272Termination Proofs by Context-Dependent Interpretations
Auteurs : Dieter Hofbauer [Allemagne]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: Proving termination of a rewrite system by an interpretation over the natural numbers directly implies an upper bound on the derivational complexity of the system. In this way, however, the derivation height of terms is often heavily overestimated. Here we present a generalization of termination proofs by interpretations that can avoid this drawback of the traditional approach. A number of simple examples illustrate how to achieve tight or even optimal bounds on the derivation height. The method is general enough to capture cases where simplification orderings fail.
Url:
DOI: 10.1007/3-540-45127-7_10
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 003088
- to stream Istex, to step Curation: 003049
- to stream Istex, to step Checkpoint: 001E13
- to stream Main, to step Merge: 009793
- to stream Main, to step Curation: 009271
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Termination Proofs by Context-Dependent Interpretations</title><author><name sortKey="Hofbauer, Dieter" sort="Hofbauer, Dieter" uniqKey="Hofbauer D" first="Dieter" last="Hofbauer">Dieter Hofbauer</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:CDC40FAF4A3DEAFD5C024DF3C31F3A7AAF18CF3A</idno><date when="2001" year="2001">2001</date><idno type="doi">10.1007/3-540-45127-7_10</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-2G0RTB9K-H/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003088</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003088</idno><idno type="wicri:Area/Istex/Curation">003049</idno><idno type="wicri:Area/Istex/Checkpoint">001E13</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001E13</idno><idno type="wicri:doubleKey">0302-9743:2001:Hofbauer D:termination:proofs:by</idno><idno type="wicri:Area/Main/Merge">009793</idno><idno type="wicri:Area/Main/Curation">009271</idno><idno type="wicri:Area/Main/Exploration">009271</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Termination Proofs by Context-Dependent Interpretations</title><author><name sortKey="Hofbauer, Dieter" sort="Hofbauer, Dieter" uniqKey="Hofbauer D" first="Dieter" last="Hofbauer">Dieter Hofbauer</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Fachbereich 17 Mathematik/Informatik, Universität Gh Kassel, D-34109, Kassel</wicri:regionArea><placeName><region type="land" nuts="1">Hesse (Land)</region><region type="district" nuts="2">District de Kassel</region><settlement type="city">Cassel (Hesse)</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Allemagne</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Proving termination of a rewrite system by an interpretation over the natural numbers directly implies an upper bound on the derivational complexity of the system. In this way, however, the derivation height of terms is often heavily overestimated. Here we present a generalization of termination proofs by interpretations that can avoid this drawback of the traditional approach. A number of simple examples illustrate how to achieve tight or even optimal bounds on the derivation height. The method is general enough to capture cases where simplification orderings fail.</div></front></TEI><affiliations><list><country><li>Allemagne</li></country><region><li>District de Kassel</li><li>Hesse (Land)</li></region><settlement><li>Cassel (Hesse)</li></settlement></list><tree><country name="Allemagne"><region name="Hesse (Land)"><name sortKey="Hofbauer, Dieter" sort="Hofbauer, Dieter" uniqKey="Hofbauer D" first="Dieter" last="Hofbauer">Dieter Hofbauer</name></region><name sortKey="Hofbauer, Dieter" sort="Hofbauer, Dieter" uniqKey="Hofbauer D" first="Dieter" last="Hofbauer">Dieter Hofbauer</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 009271 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 009271 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:CDC40FAF4A3DEAFD5C024DF3C31F3A7AAF18CF3A
|texte= Termination Proofs by Context-Dependent Interpretations
}}
| This area was generated with Dilib version V0.6.33. |  |